docs: record measured state of play, for humans and for machines - #148
Conversation
![gitar-bot[bot]](https://avatars.githubusercontent.com/in/827041?s=60&v=4){kind=small}
|
Note Automatic reviews are paused because your trial's included automatic processing has been used for this period. Upgrade now, or comment "Gitar review" to run a review anytime. Code Review ✅ Approved 1 resolved / 1 findingsAdds a measured state-of-play documentation snapshot and updates machine-readable state files to eliminate stale assertions. Consider reconciling the integration test count discrepancies noted in the findings.
✅ 1 resolved✅ Quality: Integration-test counts don't reconcile: 32 tests vs 2+27=29
OptionsDisplay: compact → Showing less information. Comment with these commands to change the behavior for this request:
Important Your trial ends in 7 days — upgrade now to keep code review, CI analysis, auto-apply, custom automations, and more. Was this helpful? React with 👍 / 👎 | Gitar |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
Adds docs/STATE-OF-PLAY-2026-07-29.adoc and brings the machine-readable .machine_readable/6a2/STATE.a2ml up to date. Both were measured on 2026-07-29 against origin/main 7d964ee and absolute-zero 87902bb7 — no figure here is recalled or inferred. STATE.a2ml had drifted since its 2026-06-12 checkpoint. Corrected: - testing-status said "ALL PASS as of 2026-04-04" and 26 aletheia unit tests. Now 29 pass, and the 27 failing integration tests are recorded explicitly as expected-by-design with the reason (they assert on stdout substrings, so they are a UI contract, not a specification). - blockers.root-justfile said the recipes are placeholders. Fixed in #144. - proof-debt cited 80 Coq Axiom/Admitted markers. That is estate/vendored scope; absolute-zero itself measures 0 Admitted and 23 Axiom. New sections in STATE.a2ml: [ci-status], [gating-reality], [proof-state], [recent-work-2026-07], [incidents], [open-questions], [landmines]. Verified to parse as TOML (`yq -p toml`), all 14 sections. The human document covers the same ground with the reasoning attached: what is actually gated (and the fact that aletheia/.github/workflows/ is inert, which let this crate stay uncompilable for over a month), the proof state, the four open questions that need a human ruling, and the landmines. README.md gains a short measured status block plus the warning about inert nested workflows, and links both documents. TEST-NEEDS.md: unit count 26 -> 29, and the note on the 27 integration failures expanded to say why they must not be "fixed" by writing checks that emit the expected strings — that would invent a definition of RSR compliance while one already exists in the estate. Verified: `asciidoctor -o /dev/null` renders with no warnings; `yq -p toml` parses STATE.a2ml in full. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Rebased onto current main and brought the two documents back into agreement
with reality. All figures re-checked; none needed changing.
- OSSF Scorecard is now PASS. It was dying at checkout on the stray gitlink;
#145 merged and it has been green on main since. Recorded, with the reason
it could not be proven on the PR: scorecard.yml triggers only on
push-to-main / schedule / workflow_dispatch, never on pull_request.
- #145 marked MERGED rather than open.
New landmine, found while re-baselining: **a merged PR can change nothing.**
Both #146 ("ci(codeql): cron weekly→monthly") and #147 ("Worktree maa ci
repair") are empty — `git diff` between their parents and merge commits is
completely blank. #146's stated change was already present; codeql.yml has read
`cron: '0 6 1 * *'` (monthly) since before it merged.
This is the sibling of the landmine already recorded above it. That one says a
merged PR may not contain the work you pushed; this one says a merged PR may not
contain any work at all. A PR title is not evidence the change happened —
check `git diff --stat <parent> <merge>`.
Verified: asciidoctor renders clean; `yq -p toml` parses STATE.a2ml in full.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
ecaea96 to
16a836a
Compare
✅ All code review findings resolved.
1 participant
Documentation only — no behaviour change. Every figure was measured on 2026-07-29 against
origin/main7d964eeandabsolute-zero87902bb7. Nothing here is recalled or inferred.New
docs/STATE-OF-PLAY-2026-07-29.adoc— human-readable snapshot: CI status, what is actually gated, aletheia's real shape, proof state, recent incidents, the open questions needing a human ruling, and the landmines to read before touching CI or history here.Updated
.machine_readable/6a2/STATE.a2mlHad drifted since its 2026-06-12 checkpoint. Corrections:
test-result = "ALL PASS as of 2026-04-04", 26 aletheia unit testsblockers.root-justfile = "recipes are placeholders"proof-debtcited 80 CoqAxiom/Admittedabsolute-zeroitself is 0Admitted, 23AxiomNew sections:
[ci-status],[gating-reality],[proof-state],[recent-work-2026-07],[incidents],[open-questions],[landmines].README.mdShort measured status block, the two known gaps (#124/#125) framed as by design, not regression, a warning that
aletheia/.github/workflows/is inert, and links to both documents.TEST-NEEDS.mdUnit count 26 → 29. The note on the 27 integration failures expanded to say why they must not be "fixed" by writing checks that emit the expected strings — that would invent a definition of RSR compliance and encode it as canonical, while one already exists (hypatia's
rsr-conformanceoracle).The through-line
Three of these files previously asserted something false about the code. That is not cosmetic: a stale
CLAUDE.mdis what tells the next agent "don't split into modules" about a crate that has been 5 modules for months, and aPROOF-NEEDS.mdthat counts onlyAdmittedmisses 23Axioms — which pass a "nosorry/Admitted" gate silently.Verification
🤖 Generated with Claude Code